 ############################################################################
 # GRAMMAR FOR NATURAL PROOF EXPRESSIONS                                    #
 #                                                                          #
 # Refer to SEMPRE's documentation for general indications on rule          #
 # construction.                                                            #
 #                                                                          #
 # Currently, domain knowledge comes from two sources. The lassie.lexicon   #
 # file contains component names (e.g. fs) and with their types             #
 # (e.g. thmlist->tactic, used for sound applications). Features of those   #
 # components (e.g. their natural name, their class/type) are read from     #
 # lassie.db into the TacticWorld.                                          #
 #                                                                          #
 # TacticWorld.java holds the main semantics of Lassie's operations, as     #
 # we piggy back on the DALExecutor for handling the semantic part of       #
 # this grammar. DALExecutor interprets semantic expression in a "world"    #
 # containing "items". We superifcially follow this convention where HOL    #
 # components can be considered the "items" of our "tactic-world".          #
 #                                                                          #
 # Generally, lowercased categories (e.g. $thm, $name) correspond to        #
 # types as found in the lexicon/database. Categories which are             #
 # capitalized are intermediates between lowercased categories and the      #
 # $tactic category.                                                        #
 ############################################################################

###########################################
#           Incorporated SML types:       #
###########################################
# $tactic
# $thm
# ($thmlist)
# $thm->tactic
# $thmlist->tactic
# $tactic->tactic
# $thm->thm
# $termquotation->tactic
# $int->tactic->tactic
# $termquotation->[thm->tactic]->tactic
# $[thm->tactic]->tactic
# $termquotation*tactic->tactic
# $termquotationlist->tactic
# $termquotation->[thm->tactic]->thm->tactic
# $termquotationlist->[thm->tactic]->thm->tactic

 ################################################################
 # Define some abbreviations for calling into library functions #
 ################################################################
(def @int2string edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.int2string)
(def @app edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.app)
(def @infix edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.infix)
(def @then edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.then)
(def @then1 edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.then1)
(def @cons edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.cons)
(def @list edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.list)
(def @quote edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.quote)
(def @parens edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.parens)
(def @op edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.op)
(def @fromFeature edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.fromFeature)
(def @intersect edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.intersect)
(def @set2string edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.set2string)
(def @choice edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.choice)
(def @tactic edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.tactic)
(def @command edu.stanford.nlp.sempre.interactive.lassie.TacticWorld.command)

(def @ChoiceFn edu.stanford.nlp.sempre.interactive.lassie.ChoiceFn)

(def @appT1T2 (lambda t1 (lambda t2 (call @app (var t1) (var t2)))))
(def @infixT1T2T3 (lambda t1 (lambda t2 (lambda t3 (call @op (var t2) (var t1) (var t3))))))

###################################
# GRAMMAR SUPPORTING LITERAL HOL4 #
###################################

(rule $ROOT ($tactic) (IdentityFn) (anchored 1))

###############################################################
##      literal SML objects, looked up from the database      #
###############################################################
## tactics
(rule $tactic
  ($TOKEN)
  (call @tactic (SimpleLexiconFn (type "tactic"))) (anchored 1))

# The root is always a tactic or a command
#(rule $ROOT ($tactic) (IdentityFn) (anchored 1))
#(rule $ROOT ($command) (lambda c (call @command (var c))) (anchored 1))
#
## Tactics can be produced by combining different constructs
#(for @category
#    (($thm->tactic $thm) ($tactic->tactic $tactic) ($thmlist->tactic $thmlist)
#     ($termquotation->tactic $termquotation)
#     ($[thm->tactic]->tactic $thm->tactic))
#  (rule $tactic @category @appT1T2 (anchored 1)))
#(rule $tactic ($termquotation $termquotation*tactic->tactic $tactic) @infixT1T2T3 (anchored 1))
## Support for inline THEN
#(rule $tactic ($tactic $tactic->tactic->tactic $tactic) @infixT1T2T3 (anchored 1))
#
## Partial applications for things like qpat_x_assum or first_x_assum
#(rule $[thm->tactic]->tactic
#  ($termquotation->[thm->tactic]->tactic $termquotation) @appT1T2 (anchored 1))
#(rule $[thm->tactic]->thm->tactic
#  ($termquotation->[thm->tactic]->thm->tactic $termquotation) @appT1T2 (anchored 1))
#(rule $[thm->tactic]->thm->tactic
#  ($termquotationlist->[thm->tactic]->thm->tactic $termquotationlist) @appT1T2 (anchored 1))
#(rule $thm->tactic ($[thm->tactic]->thm->tactic $thm->tactic) @appT1T2 (anchored 1))
#(rule $tactic->tactic ($int->tactic->tactic $int) @appT1T2 (anchored 1))
#
## We can put parentheses around a tactic or a command
#(for @cat ($ROOT $command $tactic)
#     (rule @cat (\( @cat \)) (lambda t (call @parens (var t))) (anchored 1)))
#
###############################################################
##      literal SML objects, looked up from the database      #
###############################################################
## tactic modifiers
#(rule $tactic->tactic
#  ($TOKEN)
#  (SimpleLexiconFn (type "tactic->tactic")) (anchored 1))
## thm tactics
#(rule $thm->tactic
#  ($TOKEN)
#  (SimpleLexiconFn (type "thm->tactic") (anchored 1)))
## thm list tactics:
#(rule $thmlist->tactic
#  ($TOKEN)
#  (SimpleLexiconFn (type "thmlist->tactic") (anchored 1)))
## tactic combinators
#(rule $tactic->tactic->tactic
#  ($TOKEN)
#  (SimpleLexiconFn (type "tactic->tactic->tactic") (anchored 1)))
## term tactics
#(rule $termquotation->tactic
#  ($TOKEN)
#  (SimpleLexiconFn (type "termquotation->tactic") (anchored 1)))
## first_x_assum, last_x_assum, ...
#(rule $[thm->tactic]->tactic
#  ($TOKEN)
#  (SimpleLexiconFn (type "[thm->tactic]->tactic") (anchored 1)))
## qspec
#(rule $termquotation->[thm->tactic]->thm->tactic
#  ($TOKEN)
#  (SimpleLexiconFn (type "termquotation->[thm->tactic]->thm->tactic") (anchored 1)))
## qspecl
#(rule $termquotationlist->[thm->tactic]->thm->tactic
#  ($TOKEN)
#  (SimpleLexiconFn (type "termquotationlist->[thm->tactic]->thm->tactic") (anchored 1)))
## qpat_x_assum, qpat_assum, ...
#(rule $termquotation->[thm->tactic]->tactic
#  ($TOKEN)
#  (SimpleLexiconFn (type "termquotation->[thm->tactic]->tactic")) (anchored 1))
## ntac
#(rule $int->tactic->tactic
#      ($TOKEN)
#      (SimpleLexiconFn (type "int->tactic->tactic")) (anchored 1))
#(rule $termquotation*tactic->tactic
#      ($TOKEN)
#      (SimpleLexiconFn (type "termquotation*tactic->tactic")) (anchored 1))
#(rule $thm->thm
#  ($TOKEN)
#  (SimpleLexiconFn (type "thm->thm")) (anchored 1))
#
##### HOL4 Terms
#(rule $termquotation (` $term ') (lambda e (call @quote (var e))) (anchored 1))
#(rule $termquotation (' $term ') (lambda e (call @quote (var e))) (anchored 1))
#(rule $term ($PHRASE) (IdentityFn) (anchored 1))
#(rule $term ($term and $term) (lambda t1 (lambda t2 (call @op (string "∧") (var t1) (var t2)))) (anchored 1))
#(rule $term ($term or $term) (lambda t1 (lambda t2 (call @op (string "∨") (var t1) (var t2)))) (anchored 1))
#
#(rule $Terms ($termquotation) (IdentityFn) (anchored 1))
#(rule $Terms ($termquotation , $Terms) (lambda t1 (lambda t2 (call @cons (var t1) (var t2)))) (anchored 1))
#(rule $termquotationlist ([ $Terms ]) (lambda termquotations (call @list (var termquotations))) (anchored 1))
#(rule $termquotationlist ([ ]) (ConstantFn (call @list (string " "))) (anchored 1))
#(rule $termquotationlist ([]) (ConstantFn (call @list (string " "))) (anchored 1))
#
##### HOL4 Theorems
#(rule $thm ($thm->thm $thm) @appT1T2 (anchored 1))
#(rule $thm ($TOKEN) (IdentityFn) (anchored 1))
#
### Lists
#(rule $Thms ($thm) (IdentityFn) (anchored 1))
#(rule $Thms ($thm , $Thms) (lambda t1 (lambda t2 (call @cons (var t1) (var t2)))) (anchored 1))
#(rule $thmlist ([ $Thms ]) (lambda thms (call @list (var thms))) (anchored 1))
#(rule $thmlist ([]) (ConstantFn (call @list (string " "))) (anchored 1))
#(rule $thmlist ([ ]) (ConstantFn (call @list (string " "))) (anchored 1))
#
#
###Commands to the interactive prove interface
#(rule $command
#      (back)
#      (ConstantFn (string "(b)")) (anchored 1))
#
### Other
#(rule $Number ($TOKEN) (NumberFn) (anchored 1))
#(rule $int ($Number) (lambda n (call @int2string (var n))) (anchored 1))
#
#################################################################
### GRAMMAR SUPPORTING ABSTRACT DESCRIPTIONS OF HOL4 COMPONENTS #
#################################################################
#
### Sets and their intersections, by constructing imperative sentences
#
### Lexemes
##(rule $type_lx ($PHRASE) (SimpleLexiconFn (type type)) (anchored 1))
##(rule $name_lx ($PHRASE) (SimpleLexiconFn (type name)) (anchored 1))
##(rule $AV_lx ($PHRASE) (SimpleLexiconFn (type AV)) (anchored 1))
##(rule $VP_lx ($PHRASE) (SimpleLexiconFn (type VP)) (anchored 1))
##(rule $OBJ_lx ($PHRASE) (SimpleLexiconFn (type OBJ)) (anchored 1))
##(rule $CP_lx ($PHRASE) (SimpleLexiconFn (type CP)) (anchored 1))
##(rule $PREARG_lx ($PHRASE) (SimpleLexiconFn (type PREARG)) (anchored 1))
##
##(rule $set_lx ($PHRASE) (SimpleLexiconFn (type set)) (anchored 1))
##
#### Get sets
##(def @fromFeatureX (lambda x (call @fromFeature (var x))))
##(rule $type ($type_lx) @fromFeatureX (anchored 1))
##(rule $name ($name_lx) @fromFeatureX (anchored 1))
##(rule $AV ($AV_lx) @fromFeatureX (anchored 1))
##(rule $VP ($VP_lx) @fromFeatureX (anchored 1))
##(rule $OBJ ($OBJ_lx) @fromFeatureX (anchored 1))
##(rule $CP ($CP_lx) @fromFeatureX (anchored 1))
##(rule $PREARG ($PREARG_lx) @fromFeatureX (anchored 1))
##
##(rule $set ($set_lx) @fromFeatureX (anchored 1))
##
#### Syntactically correct intersections
##(def @intersectS1S2 (lambda s1 (lambda s2 (call @intersect (var s1) (var s2)))))
##(rule $VP ($AV $VP) @intersectS1S2 (anchored 1))
##(rule $VP ($VP $OBJ) @intersectS1S2 (anchored 1))
##(rule $VP ($VP $CP) @intersectS1S2 (anchored 1))
##(rule $VP ($VP $AV) @intersectS1S2 (anchored 1))
##
##(for @p (on with the)
##     (rule $Prep (@p) (ConstantFn null) (anchored 1)))
##(rule $set ($set $set) @intersectS1S2 (anchored 1))
##
##(for @a (use apply)
##     (rule $Apply (@a) (ConstantFn null) (anchored 1)))
##
##(rule $VP' ($Apply $name) (SelectFn 1) (anchored 1))
##(rule $VP' ($name) (IdentityFn) (anchored 1))
##(rule $VP' ($VP' $type) @intersectS1S2 (anchored 1))
##(rule $VP' ($type $VP') @intersectS1S2 (anchored 1))
##(rule $VP' ($VP) (IdentityFn) (anchored 1))
##(rule $VP' ($VP' $PREARG) @intersectS1S2 (anchored 1))
##(rule $VP' ($VP' with) (SelectFn 0) (anchored 1))
##
#### Collapsing sets to single components
##(rule $tactic' ($VP') (lambda s (call @choice (call @intersect (var s) (call @fromFeature "type.tactic")))) (anchored 1))
##(rule $tactic ($tactic') (interactive.lassie.ChoiceFn) (anchored 1))
##
##(rule $thm->tactic' ($VP') (lambda s (call @choice (call @intersect (var s) (call @fromFeature "type.thm -> tactic")))) (anchored 1))
##(rule $thm->tactic ($thm->tactic') (interactive.lassie.ChoiceFn) (anchored 1))
##
##(rule $thmlist->tactic' ($VP') (lambda s (call @choice (call @intersect (var s) (call @fromFeature "type.thm list -> tactic")))) (anchored 1))
##(rule $thmlist->tactic ($thmlist->tactic') (interactive.lassie.ChoiceFn) (anchored 1))
##
##(rule $tactic->tactic' ($VP') (lambda s (call @choice (call @intersect (var s) (call @fromFeature "type.tactic -> tactic")))) (anchored 1))
##(rule $tactic->tactic ($tactic->tactic') (interactive.lassie.ChoiceFn) (anchored 1))
##
##(rule $thm->thm' ($VP') (lambda s (call @choice (call @intersect (var s) (call @fromFeature "type.thm -> thm")))) (anchored 1))
##(rule $thm->thm ($thm->thm') (interactive.lassie.ChoiceFn) (anchored 1))
##
##(rule $termquotation->tactic' ($VP') (lambda s (call @choice (call @intersect (var s) (call @fromFeature "type.term quotation -> tactic")))) (anchored 1))
##(rule $termquotation->tactic ($termquotation->tactic') (interactive.lassie.ChoiceFn) (anchored 1))
##
##(rule $int->tactic->tactic' ($VP') (lambda s (call @choice (call @intersect (var s) (call @fromFeature "type.int -> tactic -> tactic")))) (anchored 1))
##(rule $int->tactic->tactic ($int->tactic->tactic') (interactive.lassie.ChoiceFn) (anchored 1))
#
#
### Theorems
##(rule $thm' ($set) (lambda s (call @choice (call @intersect (var s) (call @fromFeature "type.thm")))) (anchored 1))
##(rule $thm ($thm') (interactive.lassie.ChoiceFn) (anchored 1))
##
### Casting sets as lists
##(rule $Thms (all $set theorems)
##      (lambda s (call @set2string (call @intersect (var s) (call @fromFeature "type.thm"))))
##      (anchored 1))
##(rule $Thms ($set theorems)
##      (lambda s (call @set2string (call @intersect (var s) (call @fromFeature "type.thm"))))
##      (anchored 1))
##(rule $Thms (all $set)
##      (lambda s (call @set2string (call @intersect (var s) (call @fromFeature "type.thm"))))
##      (anchored 1))
#
### Typed wildcards
##(rule $tactic (\( $PHRASE : tactic \)) (IdentityFn) (anchored 1))
##(rule $thm (\( $PHRASE : thm \)) (IdentityFn) (anchored 1))
##(rule $thm->tactic (\( $PHRASE : thm->tactic \)) (IdentityFn) (anchored 1))
##(rule $thmlist->tactic (\( $PHRASE : thm list -> tactic \)) (IdentityFn) (anchored 1))
##(rule $tactic->tactic (\( $PHRASE : tactic -> tactic \)) (IdentityFn) (anchored 1))
##(rule $thm->thm (\( $PHRASE : thm -> thm \)) (IdentityFn) (anchored 1))
##(rule $termquotation->tactic (\( $PHRASE : term quotation -> tactic \)) (IdentityFn) (anchored 1))
##(rule $int->tactic->tactic (\( $PHRASE : int -> tactic -> tactic \)) (IdentityFn) (anchored 1))
##(rule $termquotation->[thm->tactic]->tactic (\( $PHRASE : term quotation -> \( thm -> tactic \) -> tactic \)) (IdentityFn) (anchored 1))
##(rule $[thm->tactic]->tactic (\( $PHRASE : \( thm -> tactic \) -> tactic \)) (IdentityFn) (anchored 1))
##(rule $termquotation*tactic->tactic (\( $PHRASE : term quotation * tactic -> tactic \)) (IdentityFn) (anchored 1))
##(rule $termquotationlist->tactic (\( $PHRASE : term quotation list -> tactic \)) (IdentityFn) (anchored 1))
##(rule $termquotation->[thm->tactic]->thm->tactic (\( $PHRASE : term quotation -> \( thm -> tactic \) -> thm -> tactic \)) (IdentityFn) (anchored 1))
##(rule $termquotationlist->[thm->tactic]->thm->tactic (\( $PHRASE : term quotation list -> \( thm -> tactic \) -> thm -> tactic \)) (IdentityFn) (anchored 1))
##
###############################
### NATURAL LANGUAGE SYNONYMS #
###############################
##
### Theorem Lists
##(rule $Thms ($Thms and $Thms) (lambda t1 (lambda t2 (call @cons (var t1) (var t2)))) (anchored 1))
##(rule $thmlist (nothing) (ConstantFn []) (anchored 1))
##(rule $thmlist (empty list) (ConstantFn []) (anchored 1))
##
### Tactic composition
##(rule $tactic ($tactic then $tactic) (lambda t1 (lambda t2 (call @then (var t1) (var t2)))) (anchored 1))
##(rule $tactic ($tactic then $tactic on the first goal) (lambda t1 (lambda t2 (call @then1 (var t1) (var t2)))) (anchored 1))
##
###############
### OPTIONALS #
###############
### App
##(for @cat ($thm->tactic $thmlist->tactic $tactic->tactic $thm->thm $termquotation->tactic $int->tactic->tactic)
##     (rule @cat ($Apply @cat) (SelectFn 1) (anchored 1)))
##
### Args
##(for @cat ($tactic $thm $thmlist $termquotation)
##     (rule @cat ($Prep @cat) (SelectFn 1) (anchored 1)))
#
############ UNUSED ###########
##(rule $tactic->tactic ($int->tactic->tactic $int) @appT1T2 (anchored 1))
##(rule $[thm->tactic]->tactic ($termquotation->[thm->tactic]->tactic $termquotation) @appT1T2 (anchored 1))
##(rule $termquotation (` $PHRASE `) (lambda e (call @quote (var e))) (anchored 1))
## TODO: Necessary?
##(rule $thm
##      ($TOKEN)
##      (SimpleLexiconFn (type "thm")) (anchored 1))
##Disabled to make learning easier... See test on "repeat" in LassieTests
##(rule $thmlist ($Thms) (lambda thms (call @list (var thms))) (anchored 1))
##(rule $termquotationlist ($Terms) (lambda termquotations (call @list (var termquotations))) (anchored 1))
### Tactic composition
##(rule $tactic ($tactic THEN $tactic) (lambda t1 (lambda t2 (call @then (var t1) (var t2)))) (anchored 1))
##(rule $tactic ($tactic THEN1 $tactic) (lambda t1 (lambda t2 (call @then1 (var t1) (var t2)))) (anchored 1))
##(rule $tactic ($tactic \\ $tactic) (lambda t1 (lambda t2 (call @then (var t1) (var t2)))) (anchored 1))
##(rule $tactic ($tactic >- $tactic) (lambda t1 (lambda t2 (call @then1 (var t1) (var t2)))) (anchored 1))
##
